<html>
<head><meta charset="utf-8"><title>static vs dynamic dependent typing · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html">static vs dynamic dependent typing</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="218127772"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218127772" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218127772">(Nov 27 2020 at 20:41)</a>:</h4>
<p>I was chatting with <span class="user-mention" data-user-id="216206">@lcnr</span> about const generics + property-based testing (<a href="https://github.com/AltSysrq/proptest/issues/219">example</a>). One piece of code we came up with was:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">struct</span> <span class="nc">Example</span><span class="o">&lt;</span><span class="k">const</span><span class="w"> </span><span class="n">N</span>: <span class="kt">usize</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="cm">/* elided */</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="k">impl</span><span class="o">&lt;</span><span class="k">const</span><span class="w"> </span><span class="n">N</span>: <span class="kt">usize</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Example</span><span class="o">&lt;</span><span class="n">N</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">fn</span> <span class="nf">new</span><span class="p">()</span><span class="w"> </span>-&gt; <span class="nc">Self</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="cm">/* elided */</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
<span class="k">impl</span><span class="o">&lt;</span><span class="k">const</span><span class="w"> </span><span class="n">N</span>: <span class="kt">usize</span><span class="o">&gt;</span><span class="w"> </span><span class="n">SomeTrait</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">Example</span><span class="o">&lt;</span><span class="n">N</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="cm">/* elided */</span><span class="w"> </span><span class="p">}</span><span class="w"></span>

<span class="c1">// This is dependent typing</span>
<span class="k">fn</span> <span class="nf">generate</span><span class="p">(</span><span class="n">n</span>: <span class="kt">usize</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nc">Example</span><span class="o">&lt;</span><span class="n">n</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// How could you implement this?</span>
<span class="p">}</span><span class="w"></span>

<span class="c1">// Is this still called "dependent typing"?</span>
<span class="k">fn</span> <span class="nf">generate</span><span class="p">(</span><span class="n">n</span>: <span class="kt">usize</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nb">Box</span><span class="o">&lt;</span><span class="k">dyn</span><span class="w"> </span><span class="n">SomeTrait</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// How could you implement this?</span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>



<a name="218127863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218127863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218127863">(Nov 27 2020 at 20:42)</a>:</h4>
<p>I was thinking the other day about how const generics are kind of like a limited version of dependent typing. (Also I'm assuming there's more to come in your post.)</p>



<a name="218127864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218127864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218127864">(Nov 27 2020 at 20:42)</a>:</h4>
<p>It <em>feels</em> like the "dynamic dependent typing" should be possible, much like how we had <code>Box&lt;dyn Foo&gt;</code> well before we had <code>impl Foo</code>.</p>



<a name="218127899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218127899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218127899">(Nov 27 2020 at 20:43)</a>:</h4>
<blockquote>
<p>I'm assuming there's more to come in your post</p>
</blockquote>
<p>Not really; feel free to jump in at any time.</p>



<a name="218127986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218127986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218127986">(Nov 27 2020 at 20:44)</a>:</h4>
<p>I guess if I have a question (and I certainly don't have a fully-formed one) it would be: what has been discussed in this realm already?</p>



<a name="218128026"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128026" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Joshua Nelson <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128026">(Nov 27 2020 at 20:45)</a>:</h4>
<p>(playground: <a href="https://play.rust-lang.org/?version=nightly&amp;mode=debug&amp;edition=2018&amp;gist=31bda78dc66f8d143c55a8d51beb0b1d">https://play.rust-lang.org/?version=nightly&amp;mode=debug&amp;edition=2018&amp;gist=31bda78dc66f8d143c55a8d51beb0b1d</a>)</p>



<a name="218128032"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128032" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128032">(Nov 27 2020 at 20:45)</a>:</h4>
<p>Can there be a <code>dyn usize</code>?</p>



<a name="218128099"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128099" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128099">(Nov 27 2020 at 20:46)</a>:</h4>
<p>Well I don't know too much about const generics, but my understanding is that dependent types include non-const values</p>



<a name="218128120"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128120" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128120">(Nov 27 2020 at 20:46)</a>:</h4>
<p>Copy-pasting from the Idris website:</p>
<div class="codehilite" data-code-language="Idris"><pre><span></span><code><span class="kr">data</span> <span class="kt">Vect</span> <span class="ow">:</span> <span class="kt">Nat</span> <span class="ow">-&gt;</span> <span class="kt">Type</span> <span class="ow">-&gt;</span> <span class="kt">Type</span> <span class="kr">where</span>
    <span class="nf">Nil</span>  <span class="ow">:</span> <span class="kt">Vect</span> <span class="kt">Z</span> a
    <span class="ow">(::)</span> <span class="ow">:</span> a <span class="ow">-&gt;</span> <span class="kt">Vect</span> k a <span class="ow">-&gt;</span> <span class="kt">Vect</span> <span class="ow">(</span><span class="kt">S</span> k<span class="ow">)</span> a
</code></pre></div>
<div class="codehilite" data-code-language="Idris"><pre><span></span><code><span class="nf">app</span> <span class="ow">:</span> <span class="kt">Vect</span> n a <span class="ow">-&gt;</span> <span class="kt">Vect</span> m a <span class="ow">-&gt;</span> <span class="kt">Vect</span> <span class="ow">(</span>n <span class="ow">+</span> m<span class="ow">)</span> a
app <span class="kt">Nil</span>       ys <span class="ow">=</span> ys
app <span class="ow">(</span>x <span class="ow">::</span> xs<span class="ow">)</span> ys <span class="ow">=</span> x <span class="ow">::</span> app xs ys
</code></pre></div>



<a name="218128153"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128153" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128153">(Nov 27 2020 at 20:47)</a>:</h4>
<p>The type <code>Vect</code>  has a type! Or I guess a 'kind'?</p>



<a name="218128166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128166">(Nov 27 2020 at 20:48)</a>:</h4>
<p>I have no idea how it's implemented though</p>



<a name="218128271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128271">(Nov 27 2020 at 20:49)</a>:</h4>
<blockquote>
<p><div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="c1">// Is this still called "dependent typing"?</span>
<span class="k">fn</span> <span class="nf">generate</span><span class="p">(</span><span class="n">n</span>: <span class="kt">usize</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nb">Box</span><span class="o">&lt;</span><span class="k">dyn</span><span class="w"> </span><span class="n">SomeTrait</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="c1">// How could you implement this?</span>
<span class="p">}</span><span class="w"></span>
</code></pre></div><br>
</p>
</blockquote>
<p>Wouldn't you have to specify <code>n</code> in <code>Box&lt;dyn SomeTrait&gt;</code> somehow? I feel like this wouldn't be possible because const generics need to be <em>const</em></p>



<a name="218128466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128466">(Nov 27 2020 at 20:53)</a>:</h4>
<p>My limited understanding is that dependent types require that the concept of “type” be expressable at runtime.</p>



<a name="218128537"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128537" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128537">(Nov 27 2020 at 20:54)</a>:</h4>
<p>not necessarily <span aria-label="sweat smile" class="emoji emoji-1f605" role="img" title="sweat smile">:sweat_smile:</span></p>



<a name="218128545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128545">(Nov 27 2020 at 20:55)</a>:</h4>
<p>we could allow them at compile time only (i.e. functions that could only be called at compile time)</p>



<a name="218128625"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128625" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128625">(Nov 27 2020 at 20:56)</a>:</h4>
<p>So a <code>onlyconst fn</code></p>



<a name="218128629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128629">(Nov 27 2020 at 20:56)</a>:</h4>
<p>so my understanding is that dependent types mean that values and types can influence each other in the same context</p>



<a name="218128659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128659">(Nov 27 2020 at 20:57)</a>:</h4>
<p>Will full const generics allow <code>fn x(_: Foo&lt;thing()&gt;)</code>?</p>



<a name="218128701"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128701" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128701">(Nov 27 2020 at 20:58)</a>:</h4>
<p><code>min_const_generics</code> already allows this</p>



<a name="218128708"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128708" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128708">(Nov 27 2020 at 20:58)</a>:</h4>
<p>well <code>Foo&lt;{ thing() }&gt;</code></p>



<a name="218128721"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128721" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128721">(Nov 27 2020 at 20:58)</a>:</h4>
<p>I hesitated about the curlies</p>



<a name="218128736"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128736" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128736">(Nov 27 2020 at 20:59)</a>:</h4>
<p>always use the curlies</p>



<a name="218128740"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128740" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128740">(Nov 27 2020 at 20:59)</a>:</h4>
<p>they are your friend</p>



<a name="218128745"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128745" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128745">(Nov 27 2020 at 20:59)</a>:</h4>
<p>except when they aren't</p>



<a name="218128746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128746">(Nov 27 2020 at 20:59)</a>:</h4>
<p>in which case they are not</p>



<a name="218128830"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128830" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128830">(Nov 27 2020 at 21:00)</a>:</h4>
<p>So a <code>const fn x(n: usize) -&gt; Foo&lt;{n}&gt;)</code> isn’t conceptually distant from the current world.</p>



<a name="218128834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128834">(Nov 27 2020 at 21:00)</a>:</h4>
<p>oh that</p>



<a name="218128852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128852">(Nov 27 2020 at 21:01)</a>:</h4>
<p>that is distant <span aria-label="laughing" class="emoji emoji-1f606" role="img" title="laughing">:laughing:</span> at least from what I can tell</p>



<a name="218128879"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128879" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128879">(Nov 27 2020 at 21:01)</a>:</h4>
<p>(Different from what I said previously, I’m echoing your <code>onlyconst</code> idea)</p>



<a name="218128937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218128937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218128937">(Nov 27 2020 at 21:02)</a>:</h4>
<p>so <code>Foo&lt;{ n }&gt;</code> captures <code>n</code> from a context (word choice might not be correct but whatever) which is equal to the one it exists in itself</p>



<a name="218129077"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129077" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129077">(Nov 27 2020 at 21:04)</a>:</h4>
<p>getting this to work requires const eval to happen as the same time as typeck</p>



<a name="218129454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129454">(Nov 27 2020 at 21:12)</a>:</h4>
<p>So it’s just a bit of refactoring? 😝</p>



<a name="218129587"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129587" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129587">(Nov 27 2020 at 21:14)</a>:</h4>
<p><em>a bit</em></p>



<a name="218129644"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129644" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129644">(Nov 27 2020 at 21:15)</a>:</h4>
<p>Popping back up a bit, it feels like <code>Foo&lt;dyn usize&gt;</code> should be theoretically possible / conceptually coherent with our current <code>min_const_generic</code> (or <code>const_generic</code>) world.</p>



<a name="218129699"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129699" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129699">(Nov 27 2020 at 21:16)</a>:</h4>
<p>i am still not sure what <code>dyn usize</code> means though</p>



<a name="218129724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129724">(Nov 27 2020 at 21:16)</a>:</h4>
<p>would this require <code>Foo&lt;dyn usize&gt;</code> to contain impls for all possible values of <code>usize</code> in its vtable?</p>



<a name="218129974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129974">(Nov 27 2020 at 21:20)</a>:</h4>
<p>No, I’d expect that the vtable would be created for each concrete N</p>



<a name="218129999"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218129999" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218129999">(Nov 27 2020 at 21:21)</a>:</h4>
<p>so it's more similar to <code>Foo&lt;impl usize&gt;</code> then</p>



<a name="218130016"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218130016" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218130016">(Nov 27 2020 at 21:21)</a>:</h4>
<p>Much like the vtable is created for a concrete type when it’s made into a trait object.</p>



<a name="218130042"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218130042" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218130042">(Nov 27 2020 at 21:21)</a>:</h4>
<p>or to</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">trait</span><span class="w"> </span><span class="n">DynFoo</span><span class="w"> </span><span class="p">{]</span><span class="w"></span>

<span class="k">impl</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="w"> </span><span class="n">DynFoo</span><span class="w"> </span><span class="k">for</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="k">for</span><span class="o">&lt;</span><span class="k">const</span><span class="w"> </span><span class="n">N</span>: <span class="kt">usize</span><span class="o">&gt;</span><span class="w"> </span><span class="n">T</span>: <span class="nc">Foo</span><span class="o">&lt;</span><span class="n">N</span><span class="o">&gt;</span><span class="w"></span>
</code></pre></div>



<a name="218130131"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218130131" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lcnr <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218130131">(Nov 27 2020 at 21:23)</a>:</h4>
<p>ah so it's</p>
<div class="codehilite"><pre><span></span><code>Foo&lt;dyn usize&gt; &lt;=&gt; \exists n: usize. T: Foo&lt;N&gt;
</code></pre></div>



<a name="218132140"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218132140" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218132140">(Nov 27 2020 at 22:01)</a>:</h4>
<p>B E H O L D my macro</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="w">    </span><span class="n">macro_rules</span><span class="o">!</span><span class="w"> </span><span class="n">const_prop</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">        </span><span class="p">(</span><span class="cp">$($n</span>: <span class="nc">literal</span><span class="p">),</span><span class="o">*</span><span class="w"> </span><span class="cp">$(,</span><span class="p">)</span><span class="o">?</span><span class="p">)</span><span class="w"> </span><span class="o">=&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">            </span><span class="n">paste</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="n">proptest</span><span class="o">!</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                    </span><span class="cp">$(</span><span class="w"></span>
<span class="w">                        </span><span class="cp">#[test]</span><span class="w"></span>
<span class="w">                        </span><span class="k">fn</span> <span class="p">[</span><span class="o">&lt;</span><span class="n">doesnt_crash_</span><span class="w"> </span><span class="cp">$n</span><span class="o">&gt;</span><span class="p">](</span><span class="n">data</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">collection</span>::<span class="n">vec</span><span class="p">(</span><span class="n">num</span>::<span class="kt">u8</span>::<span class="n">ANY</span><span class="p">,</span><span class="w"> </span><span class="mi">0</span><span class="o">..</span><span class="p">(</span><span class="mi">1024</span><span class="o">*</span><span class="mi">1024</span><span class="p">)))</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                            </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">sr</span>: <span class="nc">StringRing</span><span class="o">&lt;</span><span class="p">{</span><span class="cp">$n</span><span class="p">}</span><span class="o">&gt;</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">StringRing</span>::<span class="n">new</span><span class="p">();</span><span class="w"></span>
<span class="w">                            </span><span class="kd">let</span><span class="w"> </span><span class="k">mut</span><span class="w"> </span><span class="n">data</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="o">&amp;</span><span class="n">data</span><span class="p">[</span><span class="o">..</span><span class="p">];</span><span class="w"></span>
<span class="w">                            </span><span class="n">sr</span><span class="p">.</span><span class="n">extend</span><span class="p">(</span><span class="o">&amp;</span><span class="k">mut</span><span class="w"> </span><span class="n">data</span><span class="p">).</span><span class="n">expect</span><span class="p">(</span><span class="s">"extending failed"</span><span class="p">);</span><span class="w"></span>
<span class="w">                        </span><span class="p">}</span><span class="w"></span>
<span class="w">                    </span><span class="p">)</span><span class="o">*</span><span class="w"></span>
<span class="w">                </span><span class="p">}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
<span class="w">        </span><span class="p">};</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"></span>

<span class="w">    </span><span class="n">const_prop</span><span class="o">!</span><span class="p">(</span><span class="mi">0</span><span class="p">,</span><span class="w"> </span><span class="mi">1</span><span class="p">,</span><span class="w"> </span><span class="mi">2</span><span class="p">,</span><span class="w"> </span><span class="mi">3</span><span class="p">,</span><span class="w"> </span><span class="mi">4</span><span class="p">,</span><span class="w"> </span><span class="mi">5</span><span class="p">,</span><span class="w"> </span><span class="mi">6</span><span class="p">,</span><span class="w"> </span><span class="mi">7</span><span class="p">,</span><span class="w"> </span><span class="mi">8</span><span class="p">);</span><span class="w"></span>
</code></pre></div>



<a name="218134215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218134215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218134215">(Nov 27 2020 at 22:41)</a>:</h4>
<p>What does that even <em>do</em>?</p>



<a name="218134839"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218134839" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Poliorcetics <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218134839">(Nov 27 2020 at 22:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="307537">Camelid</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218134215">said</a>:</p>
<blockquote>
<p>What does that even <em>do</em>?</p>
</blockquote>
<p>call chtulhu ?</p>



<a name="218135915"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218135915" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218135915">(Nov 27 2020 at 23:18)</a>:</h4>
<p>Like most macros, it’s not <em>that</em> bad if you take it in pieces. </p>
<p>It defines a macro that accepts zero or more comma separated literal values with an optional trailing comma. It then starts a paste context and a proptest context. Paste adds the <code>[&lt;&gt;]</code> syntax for concatenation of idents. Proptest adds the <code>for x in X</code> syntax to the test function signature.</p>



<a name="218135975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218135975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218135975">(Nov 27 2020 at 23:20)</a>:</h4>
<p>I can call this with a bunch of numbers and it copy-pastes my test functions, appending the number to the test name and using it as the const generic parameter.</p>



<a name="218135988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218135988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218135988">(Nov 27 2020 at 23:20)</a>:</h4>
<p>It’s not as powerful as actual property based tests, but at least let’s me check various parameter values.</p>



<a name="218140098"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218140098" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218140098">(Nov 28 2020 at 01:10)</a>:</h4>
<p>What does this mean though?</p>
<blockquote>
<p><div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="p">[</span><span class="o">&lt;</span><span class="n">doesnt_crash_</span><span class="w"> </span><span class="cp">$n</span><span class="o">&gt;</span><span class="p">]</span><span class="w"></span>
</code></pre></div><br>
</p>
</blockquote>



<a name="218140105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218140105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218140105">(Nov 28 2020 at 01:10)</a>:</h4>
<p>And also: is this public code that I can look at? I'm really curious about what it's for :)</p>



<a name="218140231"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218140231" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Poliorcetics <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218140231">(Nov 28 2020 at 01:15)</a>:</h4>
<p>This creates functions named <code>doesnt_crash_0</code>, <code>doesnt_crash_1</code>, ...</p>



<a name="218140243"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218140243" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Poliorcetics <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218140243">(Nov 28 2020 at 01:15)</a>:</h4>
<p>Macro hygiene prevent creation of identifiers in such way in "normal" rust</p>



<a name="218141622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218141622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218141622">(Nov 28 2020 at 01:55)</a>:</h4>
<p>Ah I <em>think</em> I understand...</p>



<a name="218148460"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218148460" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Hill <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218148460">(Nov 28 2020 at 05:10)</a>:</h4>
<p><span class="user-mention" data-user-id="307537">@Camelid</span> That syntax is parsed by the <code>paste</code> macro</p>



<a name="218164367"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218164367" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218164367">(Nov 28 2020 at 13:25)</a>:</h4>
<p><span class="user-mention silent" data-user-id="307537">Camelid</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218140105">said</a>:</p>
<blockquote>
<p>And also: is this public code that I can look at? I'm really curious about what it's for :)</p>
</blockquote>
<p>I've published it at <a href="https://github.com/shepmaster/fantastic-rotary/blob/main/src/lib.rs">https://github.com/shepmaster/fantastic-rotary/blob/main/src/lib.rs</a>, but it's super early and very untested.</p>
<p>Basically I'm playing with const generics to be used as an in-place buffer for streaming UTF-8 text for XML parsing.</p>



<a name="218164568"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218164568" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Poliorcetics <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218164568">(Nov 28 2020 at 13:31)</a>:</h4>
<blockquote>
<p>xml parsing</p>
</blockquote>
<p>Well, if you come back from that with your sanity intact, we can probably create a religion out of it</p>



<a name="218164612"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218164612" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jake Goulding <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218164612">(Nov 28 2020 at 13:32)</a>:</h4>
<p>Not my first XML rodeo :-) (<a href="https://docs.rs/sxd-document/0.3.2/sxd_document/">https://docs.rs/sxd-document/0.3.2/sxd_document/</a>; <a href="https://docs.rs/sxd-xpath/0.4.2/sxd_xpath/">https://docs.rs/sxd-xpath/0.4.2/sxd_xpath/</a>)</p>



<a name="218170713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218170713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218170713">(Nov 28 2020 at 16:24)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116155">Jake Goulding</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218127864">said</a>:</p>
<blockquote>
<p>It <em>feels</em> like the "dynamic dependent typing" should be possible, much like how we had <code>Box&lt;dyn Foo&gt;</code> well before we had <code>impl Foo</code>.</p>
</blockquote>
<p><span class="user-mention silent" data-user-id="116155">Jake Goulding</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218128466">said</a>:</p>
<blockquote>
<p>My limited understanding is that dependent types require that the concept of “type” be expressable at runtime.</p>
</blockquote>
<p>(I have a background in dependent type theory) For something to be a dependent type, it has to be able to depend on a value that has a type. That means that things like <code>Box&lt;dyn SomeTrait&gt;</code> are not dependent types, because the type itself doesn't depend on anything other than the types <code>Box</code> and <code>dyn SomeTrait</code>, which can be typechecked without caring about <code>n</code>. Const-eval is absolutely dependent typing, although IIUC the rust version has a pretty underpowered proof theory in the dependencies; in a real DTT you could write things like</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="nf">concat</span><span class="o">&lt;</span><span class="n">T</span><span class="p">,</span><span class="w"> </span><span class="k">const</span><span class="w"> </span><span class="n">N</span>: <span class="kt">usize</span><span class="p">,</span><span class="w"> </span><span class="k">const</span><span class="w"> </span><span class="n">M</span>: <span class="kt">usize</span><span class="o">&gt;</span><span class="p">(</span><span class="n">x</span>: <span class="p">[</span><span class="n">T</span><span class="p">;</span><span class="w"> </span><span class="n">N</span><span class="p">],</span><span class="w"> </span><span class="n">y</span>: <span class="p">[</span><span class="n">T</span><span class="p">;</span><span class="w"> </span><span class="n">M</span><span class="p">])</span><span class="w"> </span>-&gt; <span class="p">[</span><span class="n">T</span><span class="p">;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">M</span><span class="p">]</span><span class="w"></span>
</code></pre></div>
<p><em>without</em> any unsafe code, in such a way that no bounds checks are necessary. (That said, I'm not actually recommending this course - you will never find the bottom of that rabbit hole.)<br>
<span class="user-mention silent" data-user-id="216206">lcnr</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218129077">said</a>:</p>
<blockquote>
<p>getting this to work requires const eval to happen as the same time as typeck</p>
</blockquote>
<p>This is the fundamental tradeoff of DTT: since types and terms become mutually recursive, type checking and evaluation have to happen at the same time. Note that since this all has to happen at compile time, run time values don't actually matter here (even in a real DTT); instead you are doing symbolic evaluation, and you have to worry about additional kinds of equality like whether <code>2 * n = n + n</code> (which is true for numerals but probably not for expressions unless you specifically optimize this; and it's not really a pure optimization because every evaluation or non-evaluation choice is observable in this domain).<br>
<span class="user-mention silent" data-user-id="116155">Jake Goulding</span> <a href="#narrow/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing/near/218129644">said</a>:</p>
<blockquote>
<p>Popping back up a bit, it feels like <code>Foo&lt;dyn usize&gt;</code> should be theoretically possible / conceptually coherent with our current <code>min_const_generic</code> (or <code>const_generic</code>) world.</p>
</blockquote>
<p>I think <code>Foo&lt;dyn usize&gt;</code> makes sense, but the notation does no favors. What you want is <code>Σ n. Foo&lt;n&gt;</code> aka <code>exists n. Foo&lt;n&gt;</code>, where the sigma represents a dependent tuple of a value <code>n: usize</code> and a <code>Foo&lt;n&gt;</code>. You can think of the <code>n: usize</code> as the analogue of a typeid and <code>Foo&lt;n&gt;</code> as the vtable if you compare it to a <code>dyn Trait</code>.</p>
<p>I think proper existential types in rust would be great. They can probably be supported without full dependent types, as long as the use is localized like <code>Foo&lt;N&gt; -&gt; exists n. Foo&lt;n&gt;</code>. The hard direction is the eliminator though; if you have an <code>exists n. Foo&lt;n&gt;</code> then you can't just get a <code>Foo&lt;N&gt;</code> out because it's been erased. You can't really call a monomorphized <code>foo&lt;N&gt;(f: Foo&lt;N&gt;) -&gt; A</code> either (that is, given <code>ex: exists n. Foo&lt;n&gt;</code>, there is some primitive operation <code>unpack(ex, foo): A</code>), because you would need <em>all</em> the copies of <code>foo</code> in order to compile it. Most dependently typed programming languages will compile the existential variable to a runtime value for this purpose, which is why you often need to box everything in these languages.</p>



<a name="218186381"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/static%20vs%20dynamic%20dependent%20typing/near/218186381" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Noah Lev <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/static.20vs.20dynamic.20dependent.20typing.html#218186381">(Nov 28 2020 at 23:36)</a>:</h4>
<blockquote>
<p>Basically I'm playing with const generics to be used as an in-place buffer for streaming UTF-8 text for XML parsing.</p>
</blockquote>
<p>That sounds cool!</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>